#include "ksat.h"
#include "solver.h"

extern solver *solver_copy(solver *);

/* return value: true feasible; false infeasible */
bool solve_ksat (struct ksat *ksat)
{
	int i, j;

	solver *s;

	s = solver_new ();

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < ksat->num_clauses; i++)
	{
		veci_resize (&lits,0);
		for (j = 0; j < ksat->clause[i].k; j++)
		{
			if (ksat->clause[i].list[j] > 0)
			{
				var = ksat->clause[i].list[j];
				veci_push (&lits, toLit (var));
			}
			else if (ksat->clause[i].list[j] < 0)
			{
				var = -ksat->clause[i].list[j];
				veci_push (&lits, lit_neg (toLit (var)));
			}
		}
		begin = veci_begin (&lits);
		if (solver_addclause (s, begin, begin + veci_size (&lits)) == false)
		{
			veci_delete (&lits);
			return false;
		}
	}

	veci_delete (&lits);

	bool st;

	st = solver_simplify (s);
	if (st == true)
		st = solver_solve (s,0,0);

	solver_delete (s);

	return st;
}

/* return value: true feasible (put one solution in array list); false infeasible */
bool solve_ksat1 (struct ksat *ksat, int list[])
{
	int i, j;

	solver *s;

	s = solver_new ();

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < ksat->num_clauses; i++)
	{
		veci_resize (&lits,0);
		for (j = 0; j < ksat->clause[i].k; j++)
		{
			if (ksat->clause[i].list[j] > 0)
			{
				var =  ksat->clause[i].list[j];
				veci_push (&lits, toLit (var));
			}
			else if (ksat->clause[i].list[j] < 0)
			{
				var = -ksat->clause[i].list[j];
				veci_push (&lits, lit_neg (toLit (var)));
			}
		}
		begin = veci_begin (&lits);
		if (solver_addclause (s, begin, begin + veci_size (&lits)) == false)
		{
			veci_delete (&lits);
			return false;
		}
	}

	veci_delete (&lits);

	bool st;

	st = solver_simplify (s);
	if (st == true)
		st = solver_solve (s,0,0);

	if (st == true)
	{
		for (i = 1; i <= ksat->num_variables; i++)
		{
			if (s->model.ptr[i] == l_True)
				list[i] = 1;
			else
				list[i] = 0;
		}
	}

	solver_delete (s);

	return st;
}

/* return value: true feasible (put the pattern of solutions in array list); false infeasible */
bool solve_ksat2 (struct ksat *ksat, int list[])
{
	int i, j;

	solver *s, *s2, *s3;

	s = solver_new ();

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	for (i = 0; i < ksat->num_clauses; i++)
	{
		veci_resize (&lits,0);
		for (j = 0; j < ksat->clause[i].k; j++)
		{
			if (ksat->clause[i].list[j] > 0)
			{
				var =  ksat->clause[i].list[j];
				veci_push (&lits, toLit (var));
			}
			else if (ksat->clause[i].list[j] < 0)
			{
				var = -ksat->clause[i].list[j];
				veci_push (&lits, lit_neg (toLit (var)));
			}
		}
		begin = veci_begin (&lits);
		if (solver_addclause (s, begin, begin + veci_size (&lits)) == false)
		{
			veci_delete (&lits);
			return false;
		}
	}

	bool st, st2;

	s2 = solver_copy (s);
	st = solver_simplify (s2);
	if (st == true)
		st = solver_solve (s2,0,0);

	if (st == true)
	{
		for (i = 1; i <= ksat->num_variables; i++)
		{
			if (list[i] == 0)
			{
				if (s2->model.ptr[i] == l_True)
					list[i] = 1;
				else
					list[i] = 0;
				continue;
			}

			s3 = solver_copy (s);

			veci_resize (&lits,0);
			var = i;
			if (s2->model.ptr[i] == l_True)
			{
				list[i] = 1;
				veci_push (&lits, lit_neg (toLit (var)));
			}
			else
			{
				list[i] = 0;
				veci_push (&lits, toLit (var));
			}
			begin = veci_begin (&lits);
			if (solver_addclause (s3, begin, begin + veci_size (&lits)) == true)
			{
				st2 = solver_simplify (s3);
				if (st2 == true)
					st2 = solver_solve (s3,0,0);
				if (st2 == true)
					list[i] = -1;
			}
			solver_delete (s3);
		}
	}

	veci_delete (&lits);
	solver_delete (s);
	solver_delete (s2);

	return st;
}
